{
 "metadata": {
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.7-final"
  },
  "orig_nbformat": 2,
  "kernelspec": {
   "name": "python3",
   "display_name": "DataAnalysis",
   "language": "python"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2,
 "cells": [
  {
   "source": [
    "# Ch10 分析句子的含义\n",
    "1.  自然语言的含义的表示，以及通过计算机进行处理\n",
    "2.  将意思表示无限制的语句集相关联\n",
    "3.  连接意思表示与句子的程序来存储信息"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "\n",
    "os.environ.setdefault('PROVER9', 'C:\\\\Program Files (x86)\\\\Prover9-Mace4\\\\bin-win32\\\\')\n",
    "\n",
    "import nltk\n",
    "from tools import show_subtitle, show_expr"
   ]
  },
  {
   "source": [
    "## 10.1 自然语言理解（NLU）\n",
    "### 10.1.1 查询数据库\n",
    "意思表示的理念和技术框架"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "% start S\nS[SEM=(?np + WHERE + ?vp)] -> NP[SEM=?np] VP[SEM=?vp]\nVP[SEM=(?v + ?pp)] -> IV[SEM=?v] PP[SEM=?pp]\nVP[SEM=(?v + ?ap)] -> IV[SEM=?v] AP[SEM=?ap]\nNP[SEM=(?det + ?n)] -> Det[SEM=?det] N[SEM=?n]\nPP[SEM=(?p + ?np)] -> P[SEM=?p] NP[SEM=?np]\nAP[SEM=?pp] -> A[SEM=?a] PP[SEM=?pp]\nNP[SEM='Country=\"greece\"'] -> 'Greece'\nNP[SEM='Country=\"china\"'] -> 'China'\nDet[SEM='SELECT'] -> 'Which' | 'What'\nN[SEM='City FROM city_table'] -> 'cities'\nIV[SEM=''] -> 'are'\nA -> 'located'\nP[SEM=''] -> 'in'\n"
     ]
    }
   ],
   "source": [
    "# sql语法的缺陷：\n",
    "# 1）某些语法公式不符合语法的规则\n",
    "# 2）把数据库的细节加入了语法公式中\n",
    "nltk.data.show_cfg('grammars/book_grammars/sql0.fcfg')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >query< ---------------\n",
      "What cities are located in China\n",
      "--------------- >trees< ---------------\n",
      "(S[SEM=(SELECT, City FROM city_table, WHERE, , , Country=\"china\")]\n",
      "  (NP[SEM=(SELECT, City FROM city_table)]\n",
      "    (Det[SEM='SELECT'] What)\n",
      "    (N[SEM='City FROM city_table'] cities))\n",
      "  (VP[SEM=(, , Country=\"china\")]\n",
      "    (IV[SEM=''] are)\n",
      "    (AP[SEM=(, Country=\"china\")]\n",
      "      (A[] located)\n",
      "      (PP[SEM=(, Country=\"china\")]\n",
      "        (P[SEM=''] in)\n",
      "        (NP[SEM='Country=\"china\"'] China)))))\n",
      "--------------- >answer< ---------------\n",
      "(SELECT, City FROM city_table, WHERE, , , Country=\"china\")\n",
      "--------------- >query_sql< ---------------\n",
      "SELECT City FROM city_table WHERE   Country=\"china\"\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "\n",
    "cp = load_parser('grammars/book_grammars/sql0.fcfg')\n",
    "# cp = load_parser('grammars/book_grammars/sql0.fcfg',trace = 3)\n",
    "query = 'What cities are located in China'\n",
    "trees = list(cp.parse(query.split()))\n",
    "answer = trees[0].label()['SEM']\n",
    "query_sql = ' '.join(answer)\n",
    "show_subtitle(\"query\")\n",
    "print(query)\n",
    "show_subtitle(\"trees\")\n",
    "for tree in trees:\n",
    "    print(tree)\n",
    "show_subtitle(\"answer\")\n",
    "print(answer)\n",
    "show_subtitle(\"query_sql\")\n",
    "print(query_sql)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "canton chungking dairen harbin kowloon mukden peking shanghai sian tientsin \nUsing SQL to extract rows from 'city.db' RDB.\n('athens', 'greece', 1368)\n('bangkok', 'thailand', 1178)\n('barcelona', 'spain', 1280)\n('berlin', 'east_germany', 3481)\n('birmingham', 'united_kingdom', 1112)\n('bombay', 'india', 2839)\n('brussels', 'belgium', 986)\n('bucharest', 'romania', 1237)\n('budapest', 'hungary', 1757)\n('buenos_aires', 'argentina', 3404)\n('cairo', 'egypt', 2373)\n('calcutta', 'india', 2549)\n('canton', 'china', 1496)\n('caracas', 'venezuela', 488)\n('chicago', 'united_states', 3621)\n('chungking', 'china', 1100)\n('dairen', 'china', 544)\n('delhi', 'india', 1744)\n('detroit', 'united_states', 1850)\n('glasgow', 'united_kingdom', 1090)\n('hamburg', 'west_germany', 1700)\n('harbin', 'china', 760)\n('hongkong_city', 'hongkong', 2440)\n('hyderabad', 'india', 1086)\n('istanbul', 'turkey', 1215)\n('jakarta', 'indonesia', 533)\n('johannesburg', 'south_africa', 880)\n('karachi', 'pakistan', 1126)\n('kiev', 'soviet_union', 991)\n('kobe', 'japan', 765)\n('kowloon', 'china', 547)\n('kyoto', 'japan', 1204)\n('leningrad', 'soviet_union', 2800)\n('lima', 'peru', 835)\n('london', 'united_kingdom', 8346)\n('los_angeles', 'united_states', 1970)\n('madras', 'india', 1416)\n('madrid', 'spain', 1700)\n('manila', 'philippines', 1025)\n('melbourne', 'australia', 1595)\n('mexico_city', 'mexico', 3796)\n('milan', 'italy', 1269)\n('montreal', 'canada', 1109)\n('moscow', 'soviet_union', 4800)\n('mukden', 'china', 1551)\n('nagoya', 'japan', 1337)\n('nanking', 'japan', 1020)\n('naples', 'italy', 1012)\n('new_york', 'united_states', 7795)\n('osaka', 'japan', 2547)\n('paris', 'france', 2850)\n('peking', 'china', 2031)\n('philadelphia', 'united_states', 2072)\n('pusan', 'south_korea', 474)\n('rio_de_janeiro', 'brazil', 2413)\n('rome', 'italy', 1760)\n('saigon', 'vietnam', 695)\n('santiago', 'chile', 1350)\n('sao_paulo', 'brazil', 2228)\n('seoul', 'south_korea', 1446)\n('shanghai', 'china', 5407)\n('sian', 'china', 629)\n('singapore_city', 'singapore', 1264)\n('sydney', 'australia', 1898)\n('tehran', 'iran', 1010)\n('tientsin', 'china', 1795)\n('tokyo', 'japan', 8535)\n('toronto', 'canada', 668)\n('vienna', 'austria', 1766)\n('warsaw', 'poland', 965)\n('yokohama', 'japan', 1143)\n"
     ]
    }
   ],
   "source": [
    "# NLTK Semantic Interpretation Package, SEM = Semantic\n",
    "from nltk.sem import chat80\n",
    "\n",
    "rows = chat80.sql_query('corpora/city_database/city.db', query_sql)\n",
    "for r in rows:\n",
    "    print(r[0], end = \" \")\n",
    "\n",
    "rows = chat80.sql_demo()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >query< ---------------\nWhat cities are located in China and have populations above 1,000,000\n--------------- >trees< ---------------\n(S[SEM=(SELECT, City FROM city_table, WHERE, , , Country=\"china\", AND, , Population, >, 1000)]\n  (NP[SEM=(SELECT, City FROM city_table)]\n    (Det[SEM='SELECT'] What)\n    (N[SEM='City FROM city_table'] cities))\n  (VP[SEM=(, , Country=\"china\", AND, , Population, >, 1000)]\n    (VP[SEM=(, , Country=\"china\")]\n      (IV[SEM=''] are)\n      (AP[SEM=(, Country=\"china\")]\n        (A[] located)\n        (PP[SEM=(, Country=\"china\")]\n          (P[SEM=''] in)\n          (NP[SEM='Country=\"china\"'] China))))\n    (Conj[SEM='AND'] and)\n    (VP[SEM=(, Population, >, 1000)]\n      (TV[SEM=''] have)\n      (NP[SEM=(Population, >, 1000)]\n        (N[SEM='Population'] populations)\n        (PP[SEM=(>, 1000)]\n          (P[SEM='>'] above)\n          (NP[SEM='1000'] (CardN[SEM='1000'] 1,000,000)))))))\n--------------- >answer< ---------------\n(SELECT, City FROM city_table, WHERE, , , Country=\"china\", AND, , Population, >, 1000)\n--------------- >query_sql< ---------------\nSELECT City FROM city_table WHERE   Country=\"china\" AND  Population > 1000\n"
     ]
    }
   ],
   "source": [
    "cp = load_parser('grammars/book_grammars/sql1.fcfg')\n",
    "query = 'What cities are located in China and have populations above 1,000,000'\n",
    "trees = list(cp.parse(query.split()))\n",
    "answer = trees[0].label()['SEM']\n",
    "query_sql = ' '.join(answer)\n",
    "show_subtitle(\"query\")\n",
    "print(query)\n",
    "show_subtitle(\"trees\")\n",
    "for tree in trees:\n",
    "    print(tree)\n",
    "show_subtitle(\"answer\")\n",
    "print(answer)\n",
    "show_subtitle(\"query_sql\")\n",
    "print(query_sql)"
   ]
  },
  {
   "source": [
    "### 10.1.2 自然语言、语义和逻辑\n",
    "\n",
    "语义的基本概念：\n",
    "\n",
    "1.  在确定的情况下，陈述句非真即假\n",
    "2.  名词短语和专有名词的定义指的世界上的东西\n",
    "\n",
    "语句集W的模型是某种规范化表示，其中W中的所有句子都为真。表示模型的方式通常基于集合论。\n",
    "\n",
    "模型用于评估英语句子的真假，并用这种方式来说明表示意思的一些方法"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "## 10.2 命题逻辑\n",
    "\n",
    "设计一种逻辑语言的目的是使推理更加明确规范。\n",
    "\n",
    "-   命题逻辑只表示对应的特定语句连接词的语言结构部分。\n",
    "-   命题逻辑形式中，连接词的对应形式叫做布尔运算符。\n",
    "-   命题逻辑的基本表达式是命题符号。通常写作P、Q、R等\n",
    "-   有了命题符号和布尔运算符，可以建立命题逻辑的规范公式的无限集合（简称公式）"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "negation       \t-\nconjunction    \t&\ndisjunction    \t|\nimplication    \t->\nequivalence    \t<->\n"
     ]
    }
   ],
   "source": [
    "nltk.boolean_ops()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "False\nTrue\n"
     ]
    }
   ],
   "source": [
    "# LogicParser()将逻辑表达式分析成表达式的各种子类\n",
    "read_expr = nltk.sem.Expression.fromstring\n",
    "con1=read_expr('-(P&Q)')\n",
    "con2=read_expr('P&Q')\n",
    "con3=read_expr('--(P&Q)')\n",
    "R1=read_expr('P|(R->Q)')\n",
    "R2=read_expr('P<->--P')\n",
    "prover=nltk.Prover9()\n",
    "print(prover.prove(con1,[con2,R1]))\n",
    "print(prover.prove(con3,[con2,R2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 8
    }
   ],
   "source": [
    "# 从计算的角度看，逻辑是进行推理的重要工具。从假设一步步捡到结论，被称为推理。\n",
    "# 有效的论证：所有的前提为真时，结论都为真的论证\n",
    "read_expr = nltk.sem.Expression.fromstring\n",
    "SnF = read_expr('SnF')\n",
    "NotFns = read_expr('-FnS')\n",
    "R = read_expr('SnF-> -FnS')\n",
    "prover = nltk.Prover9()\n",
    "prover.prove(NotFns, [SnF, R])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 9
    }
   ],
   "source": [
    "# 为每个命题符号分配一个值，通过查询确定布尔运算符的含义，并用它们替代这些公式的组成成分的值，来计算合成公式的值\n",
    "# 配对的链表初始化估值，每个配对由语义符号和语义值组成。\n",
    "val = nltk.Valuation([('P', True), ('Q', True), ('R', False)])\n",
    "val['P']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(P&Q)= True\n-(P&Q)= False\n(P&R)= False\n(P|R)= True\n"
     ]
    }
   ],
   "source": [
    "# dom和g参数都被忽略了，后面会用于更加复杂的模型\n",
    "dom = set()\n",
    "grammar1 = nltk.Assignment(dom)\n",
    "model1 = nltk.Model(dom, val)\n",
    "print('(P&Q)=',model1.evaluate('(P&Q)', grammar1))\n",
    "print('-(P&Q)=',model1.evaluate('-(P&Q)', grammar1))\n",
    "print('(P&R)=',model1.evaluate('(P&R)', grammar1))\n",
    "print('(P|R)=',model1.evaluate('(P|R)', grammar1))"
   ]
  },
  {
   "source": [
    "## 10.3 一阶逻辑\n",
    "通过翻译自然语言表达式成为一阶逻辑是计算语义的不错的选择"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "### 10.3.1 语法\n",
    "一阶逻辑保留了所有命题逻辑的布尔运算符。\n",
    "\n",
    "命题被分析成谓词和参数，接近于自然语言的结构的距离\n",
    "\n",
    "一阶逻辑的标准构造规则的术语：独立变量、独立常量、带不同数量的参数的谓词（一元谓词、二元谓词）\n",
    "\n",
    "表达式被称为非逻辑常量；逻辑觉得在一阶逻辑的每个模型中的解释总是相同的。\n",
    "\n",
    "通过为表达式指定类型可以检查一阶逻辑表达式的语法结构。\n",
    "\n",
    "基本类型：e是实体类型；t是公式类型，即有真值的表达式类型。\n",
    "\n",
    "给定两种基本类型，可以形成函数表达式的复杂类型。\n",
    "\n",
    "信号，作为字典实现与非逻辑变量类型之间的关联。\n",
    "\n",
    "同指称，语义上是等价的。\n",
    "\n",
    "约束，与同指称关系不同的关系。存在量词，全称量词。"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "expr= walk(angus)\nexpr.argument= angus\nexpr.argument.type= e\nexpr.function= walk\nexpr.function.type= <e,?>\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr('walk(angus)', type_check = True)\n",
    "print(\"expr=\",expr)\n",
    "print(\"expr.argument=\",expr.argument)\n",
    "print(\"expr.argument.type=\",expr.argument.type)\n",
    "print(\"expr.function=\",expr.function)\n",
    "print(\"expr.function.type=\",expr.function.type)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "expr= walk(angus)\nexpr.free()= set()\nexpr.argument= angus\nexpr.argument.type= e\nexpr.function= walk\nexpr.function.type= e\n"
     ]
    }
   ],
   "source": [
    "sig = {'walk': '<e,t>'}\n",
    "expr = read_expr('walk(angus)', signature = sig)\n",
    "print(\"expr=\",expr)\n",
    "print(\"expr.free()=\",expr.free())\n",
    "print(\"expr.argument=\",expr.argument)\n",
    "print(\"expr.argument.type=\",expr.argument.type)\n",
    "print(\"expr.function=\",expr.function)\n",
    "print(\"expr.function.type=\",expr.function.type)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "set()\n{Variable('x')}\nset()\nset()\n{Variable('x')}\n{Variable('y')}\n"
     ]
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "# free() 返回在expr中自由变量的集合\n",
    "print(read_expr('dog(cyril)').free())\n",
    "print(read_expr('dog(x)').free())\n",
    "print(read_expr('own(angus,cyril)').free())\n",
    "print(read_expr('exists x.dog(x)').free())\n",
    "print(read_expr('((some x. walk(x)) -> sing(x))').free())\n",
    "print(read_expr('exists x.own(y,x)').free())"
   ]
  },
  {
   "source": [
    "### 10.3.2 一阶定理证明"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 15
    }
   ],
   "source": [
    "NotFnS = read_expr('-north_of(f,s)')\n",
    "SnF = read_expr('north_of(s,f)')\n",
    "R = read_expr('all x. all y. (north_of(x,y) -> -north_of(y,x))')\n",
    "prover = nltk.Prover9()\n",
    "prover.prove(NotFnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "execution_count": 16
    }
   ],
   "source": [
    "FnS = read_expr('north_of(f,s)')\n",
    "prover.prove(FnS, [SnF, R])"
   ]
  },
  {
   "source": [
    "### 10.3.3 一阶逻辑语言总结\n",
    "命题逻辑的语法规则，量词的标准规则，组合成一阶逻辑语法"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "### 10.3.4 真值模型\n",
    "给定一阶逻辑语言L，L的模型M是一个<D,Val>对，其中D是一个非空集合，称为模型的域；Val是一个函数，称为估值函数。"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "{'bertie': 'b',\n 'boy': {('b',)},\n 'cyril': 'c',\n 'dog': {('c',)},\n 'girl': {('o',)},\n 'olive': 'o',\n 'see': {('o', 'c'), ('b', 'o'), ('c', 'b')},\n 'walk': {('c',), ('o',)}}\n"
     ]
    }
   ],
   "source": [
    "# NLTk的语义关系可以使用标准的集合论的方法表示：作为元组的集合。\n",
    "dom = set(['b', 'o', 'c'])\n",
    "v = \"\"\"\n",
    "bertie=>b\n",
    "olive=>o\n",
    "cyril=>c\n",
    "boy=>{b}\n",
    "girl=>{o}\n",
    "dog=>{c}\n",
    "walk=>{o,c}\n",
    "see=>{(b,o),(c,b),(o,c)}\n",
    "\"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "print(val)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "('o', 'c') in val['see']= True\n('b',) in val['boy']= True\n"
     ]
    }
   ],
   "source": [
    "print(\"('o', 'c') in val['see']=\",('o', 'c') in val['see'])\n",
    "print(\"('b',) in val['boy']=\",('b',) in val['boy'])"
   ]
  },
  {
   "source": [
    "### 10.3.5 独立变量和赋值\n",
    "在模型中，上下文对应的使用是为变量赋值。这是一个从独立变量到域中实体的映射。"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "g[c/y][o/x]\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'x': 'o', 'y': 'c'}"
      ]
     },
     "metadata": {},
     "execution_count": 19
    }
   ],
   "source": [
    "# 赋值使用Assignment()实现，以论述的模型的域为参数。\n",
    "grammar1 = nltk.Assignment(dom, [('x', 'o'), ('y', 'c')])\n",
    "print(grammar1)  # 与逻辑学课本中出现的符号类似\n",
    "grammar1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Domain = {'b', 'o', 'c'},\nValuation = \n{'bertie': 'b',\n 'boy': {('b',)},\n 'cyril': 'c',\n 'dog': {('c',)},\n 'girl': {('o',)},\n 'olive': 'o',\n 'see': {('o', 'c'), ('b', 'o'), ('c', 'b')},\n 'walk': {('c',), ('o',)}}\nTrue\nTrue\nc\nFalse\nFalse\n"
     ]
    }
   ],
   "source": [
    "# 一阶逻辑的原子公式估值\n",
    "model1 = nltk.Model(dom, val)\n",
    "print(model1)\n",
    "print(model1.evaluate('see(olive,y)', grammar1))\n",
    "print(model1.evaluate('see(olive,cyril)', grammar1))\n",
    "print(grammar1['y'])\n",
    "print(model1.evaluate('see(y,x)', grammar1))\n",
    "print(model1.evaluate('see(cyril,olive)', grammar1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{}"
      ]
     },
     "metadata": {},
     "execution_count": 21
    }
   ],
   "source": [
    "grammar1.purge()  # 清除所有的绑定\n",
    "grammar1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "True\nTrue\nTrue\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'x': 'o', 'y': 'c'}"
      ]
     },
     "metadata": {},
     "execution_count": 22
    }
   ],
   "source": [
    "grammar1 = nltk.Assignment(dom, [('x', 'o'), ('y', 'c')])\n",
    "# 确定模型中公式的真假的一般过程称为模型检查\n",
    "print(model1.evaluate('see(olive,y)', grammar1))\n",
    "print(model1.evaluate('see(olive,cyril)', grammar1))\n",
    "print(model1.evaluate('see(bertie,olive) & boy(bertie) & -walk(bertie)', grammar1))\n",
    "grammar1"
   ]
  },
  {
   "source": [
    "### 10.3.6 量化"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "True\nTrue\n"
     ]
    }
   ],
   "source": [
    "print(model1.evaluate('exists x. (girl(x) & walk(x))', grammar1))\n",
    "print(model1.evaluate('girl(x) & walk(x)', grammar1.add('x', 'o')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "metadata": {},
     "execution_count": 24
    }
   ],
   "source": [
    "fmla1 = read_expr('girl(x)|boy(x)')\n",
    "model1.satisfiers(fmla1, 'x', grammar1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'b', 'c', 'o'}"
      ]
     },
     "metadata": {},
     "execution_count": 25
    }
   ],
   "source": [
    "# 前面为真，后面也为真，公式就是真；前面为假，后面无论什么，公式都是真\n",
    "fmla2 = read_expr('girl(x)->walk(x)')\n",
    "model1.satisfiers(fmla2, 'x', grammar1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "metadata": {},
     "execution_count": 26
    }
   ],
   "source": [
    "fmla3 = read_expr('walk(x)->girl(x)')\n",
    "model1.satisfiers(fmla3, 'x', grammar1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 27
    }
   ],
   "source": [
    "model1.evaluate('all x.(girl(x) -> walk(x))', grammar1)"
   ]
  },
  {
   "source": [
    "### 10.3.7 量词范围歧义：使用两个量词规范化地表示一个语句时，可能会发生歧义"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [],
   "source": [
    "v2 = \"\"\"\n",
    "bruce=>b\n",
    "cyril=>c\n",
    "elspeth=>e\n",
    "julia=>j\n",
    "matthew=>m\n",
    "person=>{b,e,j,m}\n",
    "admire=>{(j,b),(b,b),(m,e),(e,m),(c,a)}\n",
    "\"\"\"\n",
    "val2 = nltk.Valuation.fromstring(v2)\n",
    "dom2 = val2.domain\n",
    "model2 = nltk.Model(dom2, val2)\n",
    "grammar2 = nltk.Assignment(dom2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'a', 'b', 'c', 'e', 'j', 'm'}"
      ]
     },
     "metadata": {},
     "execution_count": 29
    }
   ],
   "source": [
    "fmla4 = read_expr('(person(x)-> exists y.(person(y) & admire(x,y)))')\n",
    "model2.satisfiers(fmla4, 'x', grammar2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "metadata": {},
     "execution_count": 30
    }
   ],
   "source": [
    "fmla5 = read_expr('(person(y) & all x.(person(x) -> admire(x,y)))')\n",
    "model2.satisfiers(fmla5, 'y', grammar2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'b'}"
      ]
     },
     "metadata": {},
     "execution_count": 31
    }
   ],
   "source": [
    "fmla6 = read_expr('(person(y) & all x.((x=bruce | x=julia) -> admire(x,y)))')\n",
    "model2.satisfiers(fmla6, 'y', grammar2)"
   ]
  },
  {
   "source": [
    "### 10.3.8 模型的建立\n",
    "\n",
    "模型的建立在给定一些句子集合的条件的基础之上，尝试创建一个新的模型。\n",
    "\n",
    "如果成功，那么说明集合是一致的。\n",
    "\n",
    "调用Mace4模型生成器，将候选的句子集合作为假设，保留目标为未指定"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "True\nTrue\nFalse\n"
     ]
    }
   ],
   "source": [
    "a3 = read_expr('exists x.(man(x) & walk(x))')\n",
    "c1 = read_expr('mortal(socrates)')\n",
    "c2 = read_expr('-mortal(socrates)')\n",
    "mb = nltk.Mace(5)  # The maximum model size that Mace will try before simply returning false.\n",
    "# a3与c1一致，a3与c2一致。因为Mace成功为a3与c1建立了模型，也为a3与c2建立了模型\n",
    "# 模型建立器可以作为定理证明器的辅助\n",
    "print(mb.build_model(None, [a3, c1]))\n",
    "print(mb.build_model(None, [a3, c2]))\n",
    "print(mb.build_model(None, [c1, c2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Adam loves Eve.= True\n{'C1': 'b',\n 'adam': 'a',\n 'eve': 'a',\n 'love': {('a', 'b')},\n 'man': {('a',)},\n 'woman': {('a',), ('b',)}}\n"
     ]
    }
   ],
   "source": [
    "# 根据假设：There is a woman that every man loves, Adam is a man, Eve is a worman.\n",
    "# 推出结论：Adam loves Eve.\n",
    "a4 = read_expr('exists y.(woman(y) & all x. (man(x) -> love(x,y)))')\n",
    "a5 = read_expr('man(adam)')\n",
    "a6 = read_expr('woman(eve)')\n",
    "grammar3 = read_expr('love(adam,eve)')\n",
    "mc = nltk.MaceCommand(grammar3, assumptions = [a4, a5, a6])\n",
    "print(\"Adam loves Eve.=\",mc.build_model())\n",
    "print(mc.valuation)\n",
    "# C1是一个“Skolem常量”，模型生成器作为存在量词的表示被引入"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Adam loves Eve.= True\n{'C1': 'c',\n 'adam': 'a',\n 'eve': 'b',\n 'love': {('a', 'c')},\n 'man': {('a',)},\n 'woman': {('c',), ('b',)}}\n"
     ]
    }
   ],
   "source": [
    "# 引入新的假设 a7\n",
    "a7 = read_expr('all x. (man(x) -> -woman(x))')\n",
    "grammar4 = read_expr('love(adam,eve)')\n",
    "mc = nltk.MaceCommand(grammar4, assumptions = [a4, a5, a6, a7])\n",
    "print(\"Adam loves Eve.=\",mc.build_model())\n",
    "print(mc.valuation)"
   ]
  },
  {
   "source": [
    "## 10.4 英语语句的语义\n",
    "### 10.4.1 基于特征方法的成分语义学\n",
    "\n",
    "组合原则：整体的含义是部分的含义与它们的句法结合方式的函数。\n",
    "\n",
    "目标是以一种可以与分析过程平滑对接的方式整合语义表达的构建。\n",
    "\n",
    "λ 运算：在组装英文句子的意思表示时组合一阶逻辑表达式。"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "### 10.4.2 λ 运算\n",
    "\n",
    "λ 运算符，约束运算符，一阶逻辑量词。\n",
    "\n",
    "λ-抽象。表示动词短语（或者无主语从句），作为参数出现在自己的右侧时。\n",
    "\n",
    "开放公式 φ 有自由变量 x，x 抽象为属性表达式 λx.φ——满足 φ 的 x 的属性。\n",
    "\n",
    "β-约简：简化语言表示"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\x.(walk(x) & chew_gum(x))\nfree()= set()\n\\x.(walk(x) & chew_gum(x))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\x.(walk(x) & chew_gum(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= (walk(gerald) & chew_gum(gerald))\nfree()= set()\n\\x.(walk(x) & chew_gum(x))(gerald)\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\x.(walk(x) & chew_gum(x))(gerald)')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\y.(dog(cyril) & own(y,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x. \\y. (dog(x) & own(y,x))(cyril)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(dog(cyril) & own(angus,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x \\y (dog(x) & own(y,x))(cyril,angus)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(dog(cyril) & own(angus,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x. \\y. (dog(x) & own(y,x))(cyril,angus)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(dog(cyril) & own(angus,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x y. (dog(x) & own(y,x))(cyril,angus)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\y.dog(y)(\\x.walk(x))\ndog(\\x.walk(x))\n"
     ]
    }
   ],
   "source": [
    "# 不可以将一个 λ-抽象作为另一个 λ-抽象的参数\n",
    "# expr = read_expr(r'\\y. y(angus))')  # 不可以\n",
    "# expr = read_expr(r'\\y. y(angus) (\\x.walk(x))')  # 不可以，自由变量y的规定是e类型\n",
    "# expr = read_expr(r'\\P. P(angus) (\\x.walk(x))')  # 可以，命题符号，更高级的类型的变量抽象，如：P、Q作为<e,t>类型的变量\n",
    "expr = read_expr(r'\\y. dog(y) (\\x.walk(x))')  # 可以\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\y.see(y,x)\n\\y.see(y,z)\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "execution_count": 42
    }
   ],
   "source": [
    "# 语义等价？\n",
    "expr1 = read_expr(r'\\y.see(y,x)')\n",
    "expr2 = read_expr(r'\\y.see(y,z)')\n",
    "show_expr(expr1)\n",
    "show_expr(expr2)\n",
    "expr1.simplify()==expr2.simplify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\P.exists x.P(x,\\y.see(y,x))\n\\P.exists x.P(x,\\y.see(y,z))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "execution_count": 43
    }
   ],
   "source": [
    "# 语义等价？\n",
    "expr1 = read_expr(r'\\P.exists x.P(x)(\\y.see(y,x))')\n",
    "expr2 = read_expr(r'\\P.exists x.P(x)(\\y.see(y,z))')\n",
    "show_expr(expr1)\n",
    "show_expr(expr2)\n",
    "expr1.simplify()==expr2.simplify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.P(x)\nexists z.P(z)\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 44
    }
   ],
   "source": [
    "# α-等价，也叫字母变体。重新标记绑定的变量的过程称为α-转换。\n",
    "expr1 = read_expr('exists x.P(x)')\n",
    "expr2 = expr1.alpha_convert(nltk.sem.Variable('z'))\n",
    "show_expr(expr1)\n",
    "show_expr(expr2)\n",
    "expr1.simplify() == expr2.simplify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(\\P.exists x.P(x))(\\y.see(y,x))\nexists z1.see(z1,x)\n"
     ]
    }
   ],
   "source": [
    "# logic中的β-约简代码自动地重新标记\n",
    "expr3 = read_expr('\\P.(exists x.P(x))(\\y.see(y,x))')\n",
    "show_expr(expr3)"
   ]
  },
  {
   "source": [
    "### 10.4.3 量化的NP"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 81,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= exists x.(dog(x) & bark(x))\nfree()= set()\nexists x.(dog(x) & bark(x))\nβ-约简= \\P.exists x.(dog(x) & P(x))\nfree()= set()\n\\P.exists x.(dog(x) & P(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "execution_count": 81
    }
   ],
   "source": [
    "# 将主语的SEM值作为函数表达式，而不是参数（有时叫做类型提升）\n",
    "expr1 = read_expr(r'exists x.(dog(x) & bark(x))')\n",
    "expr2 = read_expr(r'\\P.exists x.(dog(x) & P(x))')\n",
    "show_expr(expr1)\n",
    "show_expr(expr2)\n",
    "expr1.simplify() == expr2.simplify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= exists x.(dog(x) & bark(x))\nfree()= set()\nexists x.(dog(x) & bark(x))\nβ-约简= \\P.exists x.(dog(x) & P(x))\nfree()= set()\n\\P.exists x.(dog(x) & P(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "execution_count": 80
    }
   ],
   "source": [
    "show_expr(expr1)\n",
    "show_expr(expr2)\n",
    "expr1.free() == expr2.free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\P.all x.(dog(x) -> P(x))\nset()\n\\P.all x.(dog(x) -> P(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<LambdaExpression \\P.all x.(dog(x) -> P(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 48
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.all x.(dog(x) -> P(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\Q P.exists x.(Q(x) & P(x))\nset()\n\\Q P.exists x.(Q(x) & P(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<LambdaExpression \\Q P.exists x.(Q(x) & P(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 49
    }
   ],
   "source": [
    "expr = read_expr(r'\\Q P.exists x.(Q(x) & P(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "walk(angus)\nset()\n\\P.P(angus)(\\x.walk(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression \\P.P(angus)(\\x.walk(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 50
    }
   ],
   "source": [
    "expr = read_expr(r'\\P. P(angus) (\\x.walk(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "walk(x)\n{Variable('x')}\n\\P.P(x)(\\x.walk(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression \\P.P(x)(\\x.walk(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 51
    }
   ],
   "source": [
    "expr = read_expr(r'\\P. P(x) (\\x.walk(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "walk(x)\n{Variable('x')}\n\\P.P(x)(\\y.walk(y))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression \\P.P(x)(\\y.walk(y))>"
      ]
     },
     "metadata": {},
     "execution_count": 52
    }
   ],
   "source": [
    "expr = read_expr(r'\\P. P(x) (\\y.walk(y))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\P.exists x.P(x,\\x.walk(x))\nset()\n\\P.exists x.P(x,\\x.walk(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<LambdaExpression \\P.exists x.P(x,\\x.walk(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 53
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.exists x.P(x) (\\x.walk(x))')  # 无法正确约简\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\P.exists x.P(x,\\y.walk(y))\nset()\n\\P.exists x.P(x,\\y.walk(y))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<LambdaExpression \\P.exists x.P(x,\\y.walk(y))>"
      ]
     },
     "metadata": {},
     "execution_count": 54
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.exists x.P(x) (\\y.walk(y))')  # 无法正确约简\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.walk(x)\nset()\n(\\P.exists x.P(x))(\\x.walk(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression (\\P.exists x.P(x))(\\x.walk(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 55
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P.exists x.P(x)) (\\x.walk(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.walk(x)\nset()\n(\\P.exists x.P(x))(\\x.walk(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression (\\P.exists x.P(x))(\\x.walk(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 56
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.(exists x.P(x)) (\\x.walk(x))')  # print(expr) == (\\P.exists x.P(x))(\\x.walk(x))\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.walk(x)\nset()\n(\\P.exists x.P(x))(\\y.walk(y))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression (\\P.exists x.P(x))(\\y.walk(y))>"
      ]
     },
     "metadata": {},
     "execution_count": 57
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.(exists x.P(x)) (\\y.walk(y))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.walk(x)\nset()\nexists x.\\P.P(x)(\\y.walk(y))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ExistsExpression exists x.\\P.P(x)(\\y.walk(y))>"
      ]
     },
     "metadata": {},
     "execution_count": 58
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(\\P.P(x) (\\y.walk(y)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & bark(x))\nset()\nexists x.(dog(x) & \\P.P(x)(\\x.bark(x)))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ExistsExpression exists x.(dog(x) & \\P.P(x)(\\x.bark(x)))>"
      ]
     },
     "metadata": {},
     "execution_count": 59
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(dog(x) & \\P.P(x) (\\x.bark(x)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & bark(x))\nset()\nexists x.(dog(x) & \\P.P(x)(\\y.bark(y)))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ExistsExpression exists x.(dog(x) & \\P.P(x)(\\y.bark(y)))>"
      ]
     },
     "metadata": {},
     "execution_count": 60
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(dog(x) & \\P.P(x) (\\y.bark(y)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & bark(x))\nset()\n((\\P Q.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\P Q.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 61
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P Q.exists x.(P(x) & Q(x) )) (\\x.dog(x))(\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & bark(x))\nset()\n((\\P Q.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\P Q.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 62
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P Q.exists x.(P(x) & Q(x) )) (\\x.dog(x),\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(bark(x) & dog(x))\nset()\n((\\Q P.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\Q P.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 63
    }
   ],
   "source": [
    "expr = read_expr(r'(\\Q P.exists x.(P(x) & Q(x) )) (\\x.dog(x))(\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(bark(x) & dog(x))\nset()\n((\\Q P.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\Q P.exists x.(P(x) & Q(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 64
    }
   ],
   "source": [
    "expr = read_expr(r'(\\Q P.exists x.(P(x) & Q(x) )) (\\x.dog(x),\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(bark(x) & dog(x))\nset()\n((\\P Q.exists x.(Q(x) & P(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\P Q.exists x.(Q(x) & P(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 65
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P Q.exists x.(Q(x) & P(x))) (\\x.dog(x))(\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(bark(x) & dog(x))\nset()\n((\\P Q.exists x.(Q(x) & P(x)))(\\x.dog(x)))(\\x.bark(x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression ((\\P Q.exists x.(Q(x) & P(x)))(\\x.dog(x)))(\\x.bark(x))>"
      ]
     },
     "metadata": {},
     "execution_count": 66
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P Q.exists x.(Q(x) & P(x))) (\\x.dog(x),\\x.bark(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & bark(x))\nset()\nexists x.(\\Q.Q(x)(\\x.dog(x)) & \\P.P(x)(\\x.bark(x)))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ExistsExpression exists x.(\\Q.Q(x)(\\x.dog(x)) & \\P.P(x)(\\x.bark(x)))>"
      ]
     },
     "metadata": {},
     "execution_count": 67
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(\\Q.Q(x) (\\x.dog(x)) & \\P.P(x)(\\x.bark(x)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(\\Q.Q(x) & dog(x,\\x.bark(x)))\nset()\nexists x.(\\Q.Q(x) & (\\P.P(x)(\\x.dog(x)))(\\x.bark(x)))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ExistsExpression exists x.(\\Q.Q(x) & (\\P.P(x)(\\x.dog(x)))(\\x.bark(x)))>"
      ]
     },
     "metadata": {},
     "execution_count": 68
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(\\Q.Q(x) & \\P.P(x)(\\x.dog(x),\\x.bark(x)))')  # 无法正确约简\n",
    "show_expr(expr)"
   ]
  },
  {
   "source": [
    "### 10.4.4 及物动词"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\\y.exists x.(dog(x) & chase(y,x))\nset()\n\\y.exists x.(dog(x) & chase(y,x))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<LambdaExpression \\y.exists x.(dog(x) & chase(y,x))>"
      ]
     },
     "metadata": {},
     "execution_count": 69
    }
   ],
   "source": [
    "expr = read_expr(r'\\y.exists x.(dog(x) & chase(y,x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & chase(y,x))\n{Variable('y')}\n(\\P.exists x.(dog(x) & P(x)))(\\z.chase(y,z))\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<ApplicationExpression (\\P.exists x.(dog(x) & P(x)))(\\z.chase(y,z))>"
      ]
     },
     "metadata": {},
     "execution_count": 70
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.(exists x.(dog(x) & P(x)))(\\z.chase(y,z))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= exists x.(dog(x) & chase(y,x))\nfree()= {Variable('y')}\nexists x.(dog(x) & \\P.P(x)(\\z.chase(y,z)))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'exists x.(dog(x) & \\P.P(x)(\\z.chase(y,z)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\X x.X(\\y.chase(x,y))\nfree()= set()\n\\X x.X(\\y.chase(x,y))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\X x.X(\\y.chase(x,y))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 92,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\X x.X(\\y.chase(x,y))\nfree()= set()\n\\X x.X(\\y.chase(x,y))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\X (\\x.X(\\y.chase(x,y)))')  # print(tvp)=>\\X x.X(\\y.chase(x,y))\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\P.exists x.(dog(x) & P(x))\nfree()= set()\n\\P.exists x.(dog(x) & P(x))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'\\P.exists x.(dog(x) & P(x))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\P.exists x.(dog(x) & P(x))\nfree()= set()\n\\P.exists x.(dog(x) & P(x))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P.exists x.(dog(x) & P(x)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\P.exists x.(dog(x) & P(x))\nfree()= set()\n\\P.exists x.(dog(x) & P(x))\n"
     ]
    }
   ],
   "source": [
    "expr = read_expr(r'(\\P.(exists x.(dog(x) & P(x))))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\x.exists z2.(dog(z2) & chase(x,z2))\nfree()= set()\n(\\X x.X(\\y.chase(x,y)))(\\P.exists x.(dog(x) & P(x)))\n"
     ]
    }
   ],
   "source": [
    "tvp = read_expr(r'\\X (\\x.X(\\y.chase(x,y)))')  # print(tvp)=>\\X x.X(\\y.chase(x,y))\n",
    "np = read_expr(r'(\\P.(exists x.(dog(x) & P(x))))')\n",
    "expr=nltk.ApplicationExpression(tvp,np)\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= \\x.exists z3.(dog(z3) & chase(x,z3))\nfree()= set()\n(\\X x.X(\\y.chase(x,y)))(\\P.exists x.(dog(x) & P(x)))\n"
     ]
    }
   ],
   "source": [
    "# expr = read_expr(r'(\\X x.X(\\y.chase(x,y)))\\P.exists x.(dog(x) & P(x))')  # 不能正确读入\n",
    "# expr = read_expr(r'(\\P.exists x.(dog(x) & P(x)))(\\X x.X(\\y.chase(x,y)))')  # 不能正确约简\n",
    "expr = read_expr(r'(\\X x.X(\\y.chase(x,y)))(\\P.exists x.(dog(x) & P(x)))')\n",
    "show_expr(expr)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 82,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "|.A.g.a.b.t.e.d.|\nLeaf Init Rule:\n|[-] . . . . . .| [0:1] 'Angus'\n|. [-] . . . . .| [1:2] 'gives'\n|. . [-] . . . .| [2:3] 'a'\n|. . . [-] . . .| [3:4] 'bone'\n|. . . . [-] . .| [4:5] 'to'\n|. . . . . [-] .| [5:6] 'every'\n|. . . . . . [-]| [6:7] 'dog'\nFeature Bottom Up Predict Combine Rule:\n|[-] . . . . . .| [0:1] PropN[-LOC, NUM='sg', SEM=<\\P.P(angus)>] -> 'Angus' *\nFeature Bottom Up Predict Combine Rule:\n|[-] . . . . . .| [0:1] NP[-LOC, NUM='sg', SEM=<\\P.P(angus)>] -> PropN[-LOC, NUM='sg', SEM=<\\P.P(angus)>] *\nFeature Bottom Up Predict Combine Rule:\n|[-> . . . . . .| [0:1] S[SEM=<?subj(?vp)>] -> NP[NUM=?n, SEM=?subj] * VP[NUM=?n, SEM=?vp] {?n: 'sg', ?subj: <LambdaExpression \\P.P(angus)>}\nFeature Bottom Up Predict Combine Rule:\n|. [-] . . . . .| [1:2] DTV[NUM='sg', SEM=<\\Y X x.X(\\z.Y(\\y.give(x,y,z)))>, TNS='pres'] -> 'gives' *\nFeature Bottom Up Predict Combine Rule:\n|. [-> . . . . .| [1:2] VP[NUM=?n, SEM=<?v(?obj,?pp)>] -> DTV[NUM=?n, SEM=?v] * NP[SEM=?obj] PP[SEM=?pp, +TO] {?n: 'sg', ?v: <LambdaExpression \\Y X x.X(\\z.Y(\\y.give(x,y,z)))>}\nFeature Bottom Up Predict Combine Rule:\n|. . [-] . . . .| [2:3] Det[NUM='sg', SEM=<\\P Q.exists x.(P(x) & Q(x))>] -> 'a' *\nFeature Bottom Up Predict Combine Rule:\n|. . [-> . . . .| [2:3] NP[NUM=?n, SEM=<?det(?nom)>] -> Det[NUM=?n, SEM=?det] * Nom[NUM=?n, SEM=?nom] {?det: <LambdaExpression \\P Q.exists x.(P(x) & Q(x))>, ?n: 'sg'}\nFeature Bottom Up Predict Combine Rule:\n|. . . [-] . . .| [3:4] N[NUM='sg', SEM=<\\x.bone(x)>] -> 'bone' *\nFeature Bottom Up Predict Combine Rule:\n|. . . [-] . . .| [3:4] Nom[NUM='sg', SEM=<\\x.bone(x)>] -> N[NUM='sg', SEM=<\\x.bone(x)>] *\nFeature Single Edge Fundamental Rule:\n|. . [---] . . .| [2:4] NP[NUM='sg', SEM=<\\Q.exists x.(bone(x) & Q(x))>] -> Det[NUM='sg', SEM=<\\P Q.exists x.(P(x) & Q(x))>] Nom[NUM='sg', SEM=<\\x.bone(x)>] *\nFeature Bottom Up Predict Combine Rule:\n|. . [---> . . .| [2:4] S[SEM=<?subj(?vp)>] -> NP[NUM=?n, SEM=?subj] * VP[NUM=?n, SEM=?vp] {?n: 'sg', ?subj: <LambdaExpression \\Q.exists x.(bone(x) & Q(x))>}\nFeature Single Edge Fundamental Rule:\n|. [-----> . . .| [1:4] VP[NUM=?n, SEM=<?v(?obj,?pp)>] -> DTV[NUM=?n, SEM=?v] NP[SEM=?obj] * PP[SEM=?pp, +TO] {?n: 'sg', ?obj: <LambdaExpression \\Q.exists x.(bone(x) & Q(x))>, ?v: <LambdaExpression \\Y X x.X(\\z.Y(\\y.give(x,y,z)))>}\nFeature Bottom Up Predict Combine Rule:\n|. . . . [-] . .| [4:5] P[+to] -> 'to' *\nFeature Bottom Up Predict Combine Rule:\n|. . . . [-> . .| [4:5] PP[SEM=?np, +TO] -> P[+TO] * NP[SEM=?np] {}\nFeature Bottom Up Predict Combine Rule:\n|. . . . . [-] .| [5:6] Det[NUM='sg', SEM=<\\P Q.all x.(P(x) -> Q(x))>] -> 'every' *\nFeature Bottom Up Predict Combine Rule:\n|. . . . . [-> .| [5:6] NP[NUM=?n, SEM=<?det(?nom)>] -> Det[NUM=?n, SEM=?det] * Nom[NUM=?n, SEM=?nom] {?det: <LambdaExpression \\P Q.all x.(P(x) -> Q(x))>, ?n: 'sg'}\nFeature Bottom Up Predict Combine Rule:\n|. . . . . . [-]| [6:7] N[NUM='sg', SEM=<\\x.dog(x)>] -> 'dog' *\nFeature Bottom Up Predict Combine Rule:\n|. . . . . . [-]| [6:7] Nom[NUM='sg', SEM=<\\x.dog(x)>] -> N[NUM='sg', SEM=<\\x.dog(x)>] *\nFeature Single Edge Fundamental Rule:\n|. . . . . [---]| [5:7] NP[NUM='sg', SEM=<\\Q.all x.(dog(x) -> Q(x))>] -> Det[NUM='sg', SEM=<\\P Q.all x.(P(x) -> Q(x))>] Nom[NUM='sg', SEM=<\\x.dog(x)>] *\nFeature Bottom Up Predict Combine Rule:\n|. . . . . [--->| [5:7] S[SEM=<?subj(?vp)>] -> NP[NUM=?n, SEM=?subj] * VP[NUM=?n, SEM=?vp] {?n: 'sg', ?subj: <LambdaExpression \\Q.all x.(dog(x) -> Q(x))>}\nFeature Single Edge Fundamental Rule:\n|. . . . [-----]| [4:7] PP[SEM=<\\Q.all x.(dog(x) -> Q(x))>, +TO] -> P[+TO] NP[SEM=<\\Q.all x.(dog(x) -> Q(x))>] *\nFeature Single Edge Fundamental Rule:\n|. [-----------]| [1:7] VP[NUM='sg', SEM=<\\x.all z5.(dog(z5) -> exists z4.(bone(z4) & give(x,z4,z5)))>] -> DTV[NUM='sg', SEM=<\\Y X x.X(\\z.Y(\\y.give(x,y,z)))>] NP[SEM=<\\Q.exists x.(bone(x) & Q(x))>] PP[SEM=<\\Q.all x.(dog(x) -> Q(x))>, +TO] *\nFeature Single Edge Fundamental Rule:\n|[=============]| [0:7] S[SEM=<all z5.(dog(z5) -> exists z4.(bone(z4) & give(angus,z4,z5)))>] -> NP[NUM='sg', SEM=<\\P.P(angus)>] VP[NUM='sg', SEM=<\\x.all z5.(dog(z5) -> exists z4.(bone(z4) & give(x,z4,z5)))>] *\nall z5.(dog(z5) -> exists z4.(bone(z4) & give(angus,z4,z5)))\n"
     ]
    }
   ],
   "source": [
    "# simple-sem.fcfg包含了一个用于分析和翻译简单例子的小型规则集合\n",
    "from nltk import load_parser\n",
    "\n",
    "parser = load_parser('grammars/book_grammars/simple-sem.fcfg', trace = 0)\n",
    "parser = load_parser('grammars/book_grammars/simple-sem.fcfg', trace = 2)\n",
    "sentence = 'Angus gives a bone to every dog'\n",
    "tokens = sentence.split()\n",
    "for tree in parser.parse(tokens):\n",
    "    print(tree.label()['SEM'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 83,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "语法表达：\n(S[SEM=<walk(irene)>]\n  (NP[-LOC, NUM='sg', SEM=<\\P.P(irene)>]\n    (PropN[-LOC, NUM='sg', SEM=<\\P.P(irene)>] Irene))\n  (VP[NUM='sg', SEM=<\\x.walk(x)>]\n    (IV[NUM='sg', SEM=<\\x.walk(x)>, TNS='pres'] walks)))\n语义表达：\nwalk(irene)\n语法表达：\n(S[SEM=<exists z6.(ankle(z6) & bite(cyril,z6))>]\n  (NP[-LOC, NUM='sg', SEM=<\\P.P(cyril)>]\n    (PropN[-LOC, NUM='sg', SEM=<\\P.P(cyril)>] Cyril))\n  (VP[NUM='sg', SEM=<\\x.exists z6.(ankle(z6) & bite(x,z6))>]\n    (TV[NUM='sg', SEM=<\\X x.X(\\y.bite(x,y))>, TNS='pres'] bites)\n    (NP[NUM='sg', SEM=<\\Q.exists x.(ankle(x) & Q(x))>]\n      (Det[NUM='sg', SEM=<\\P Q.exists x.(P(x) & Q(x))>] an)\n      (Nom[NUM='sg', SEM=<\\x.ankle(x)>]\n        (N[NUM='sg', SEM=<\\x.ankle(x)>] ankle)))))\n语义表达：\nexists z6.(ankle(z6) & bite(cyril,z6))\n"
     ]
    }
   ],
   "source": [
    "# interpret_sents() 用于批量地解释输入的语句列表。输出的是语法表达（synrep）和语义表达（semrep）\n",
    "sents = ['Irene walks', 'Cyril bites an ankle']\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "for results in nltk.interpret_sents(sents, grammar_file):\n",
    "    for (synrep, semrep) in results:\n",
    "        print(\"语法表达：\")\n",
    "        print(synrep)\n",
    "        print(\"语义表达：\")\n",
    "        print(semrep)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 84,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "(S[SEM=<all z7.(boy(z7) -> see(cyril,z7))>]\n  (NP[-LOC, NUM='sg', SEM=<\\P.P(cyril)>]\n    (PropN[-LOC, NUM='sg', SEM=<\\P.P(cyril)>] Cyril))\n  (VP[NUM='sg', SEM=<\\x.all z7.(boy(z7) -> see(x,z7))>]\n    (TV[NUM='sg', SEM=<\\X x.X(\\y.see(x,y))>, TNS='pres'] sees)\n    (NP[NUM='sg', SEM=<\\Q.all x.(boy(x) -> Q(x))>]\n      (Det[NUM='sg', SEM=<\\P Q.all x.(P(x) -> Q(x))>] every)\n      (Nom[NUM='sg', SEM=<\\x.boy(x)>]\n        (N[NUM='sg', SEM=<\\x.boy(x)>] boy)))))\nall z7.(boy(z7) -> see(cyril,z7))\nTrue\n"
     ]
    }
   ],
   "source": [
    "# evaluate_sents() 用于批量地评估输入的语句列表，输出的是语法表达（synrep）、语义表达（semrep）和真值(value)\n",
    "v = \"\"\"\n",
    "bertie=>b\n",
    "olive=>o\n",
    "cyril=>c\n",
    "boy=>{b}\n",
    "girl=>{o}\n",
    "dog=>{c}\n",
    "walk=>{o,c}\n",
    "see=>{(b,o),(c,b),(o,c)}\n",
    "\"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "grammar = nltk.Assignment(val.domain)\n",
    "model = nltk.Model(val.domain, val)\n",
    "sent = 'Cyril sees every boy'\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "results = nltk.evaluate_sents([sent], grammar_file, model, grammar)[0]\n",
    "for (synrep, semrep, value) in results:\n",
    "    print(synrep)\n",
    "    print(semrep)\n",
    "    print(value)"
   ]
  },
  {
   "source": [
    "### 10.4.5 量词歧义（同一个句子的不同的量词表示，可以跳过）\n",
    "\n",
    "在语义表示与句法分析紧密耦合的前提下，语义中量词的范围也反映了句法分析树中对应的NP的相对范围。\n",
    "\n",
    "Cooper存储：是由“核心”语义表示与绑定操作符链表组成的配对。\n",
    "\n",
    "S-检索：结合了绑定操作符与核心的操作。\n",
    "\n",
    "建立一个“核心+存储表示”的组合\n"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 85,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "chase(z2,z3)\nbo(\\P.all x.(girl(x) -> P(x)),z2)\nbo(\\P.exists x.(dog(x) & P(x)),z3)\n"
     ]
    }
   ],
   "source": [
    "# nltk.sem.cooper_storage将存储形式的语义表示转换成标准逻辑形式\n",
    "from nltk.sem import cooper_storage as cs\n",
    "\n",
    "sentence = 'every girl chases a dog'\n",
    "trees = cs.parse_with_bindops(sentence, grammar = 'grammars/book_grammars/storage.fcfg')\n",
    "semrep = trees[0].label()['SEM']\n",
    "cs_semrep = cs.CooperStore(semrep)\n",
    "print(cs_semrep.core)\n",
    "for bo in cs_semrep.store:\n",
    "    print(bo)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 86,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Permutation 1\n   (\\P.all x.(girl(x) -> P(x)))(\\z2.chase(z2,z3))\n   (\\P.exists x.(dog(x) & P(x)))(\\z3.all x.(girl(x) -> chase(x,z3)))\nPermutation 2\n   (\\P.exists x.(dog(x) & P(x)))(\\z3.chase(z2,z3))\n   (\\P.all x.(girl(x) -> P(x)))(\\z2.exists x.(dog(x) & chase(z2,x)))\n"
     ]
    }
   ],
   "source": [
    "# 检索与恢复语义表示为标准逻辑形式\n",
    "cs_semrep.s_retrieve(trace = True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x.(dog(x) & all z10.(girl(z10) -> chase(z10,x)))\nall x.(girl(x) -> exists z11.(dog(z11) & chase(x,z11)))\n"
     ]
    }
   ],
   "source": [
    "# 两种标准逻辑形式（存在量词形式、全称量词形式）\n",
    "for reading in cs_semrep.readings:\n",
    "    print(reading)"
   ]
  },
  {
   "source": [
    "## 10.5 段落（话语）语义\n",
    "\n",
    "段落是语句的序列。组成段落的句子的解释依赖于它前面的句子。\n",
    "\n",
    "照应代词（anaphoric pronouns），即回指代词"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "### 10.5.1 段落表示理论（Discourse Representation Theory，DRT），即话语表示理论。\n",
    "\n",
    "一阶逻辑中的量化标准方法仅限于单个句子，下面介绍可以扩大到多个句子的方法。\n",
    "-   段落表示理论的目标是提供处理多个句子以及其他段落特征的语义现象的方法。\n",
    "-   段落表示结构（Discourse Representation Structure，DRS）根据一个段落指称的列表和一个条件列表表示段落的意思。\n",
    "-   段落指称是段落中正在讨论的事情，对应于一阶逻辑中的单个变量\n",
    "-   段落表示结构的条件应用于段落指称，对应于一阶逻辑中的原子开放公式。\n"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 89,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,y],[angus(x), dog(y), own(x,y)])\nfree()= set()\n([x,y],[angus(x), dog(y), own(x,y)])\n"
     ]
    }
   ],
   "source": [
    "read_dexpr = nltk.sem.DrtExpression.fromstring\n",
    "drs1 = read_dexpr('([x,y],[angus(x),dog(y),own(x,y)])')\n",
    "show_expr(drs1)\n",
    "drs1.draw()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 90,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "exists x y.(angus(x) & dog(y) & own(x,y))\n"
     ]
    }
   ],
   "source": [
    "# 使用fol()函数，可以把每一个段落表示结构都可以转化为一阶逻辑公式\n",
    "print(drs1.fol())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 93,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,y],[walk(x), run(y)])\nfree()= set()\n(([x],[walk(x)]) + ([y],[run(y)]))\n"
     ]
    }
   ],
   "source": [
    "# DRT表达式中可以使用DRS连接运算符（“+”）\n",
    "# DRS连接是指一个单独的DRS包含合并的段落指称和来自多个论证的条件\n",
    "# DRS连接可以通过α-转换（simplify()）自动完成\n",
    "drs2 = read_dexpr('([x],[walk(x)])+([y],[run(y)])')\n",
    "show_expr(drs2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 94,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,y],[walk(x), run(y), see(x,y)])\nfree()= {Variable('x')}\n(([x],[walk(x)]) + ([y],[run(y), see(x,y)]))\n(exists x.walk(x) & exists y.(run(y) & see(x,y)))\n"
     ]
    }
   ],
   "source": [
    "drs2 = read_dexpr('([x],[walk(x)])+([y],[run(y),see(x,y)])')\n",
    "show_expr(drs2)\n",
    "print(drs2.fol())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 95,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,y,z],[walk(x), run(y), see(x,z)])\nfree()= {Variable('x')}\n(([x],[walk(x)]) + ([y],[run(y)]) + ([z],[see(x,z)]))\n(exists x.walk(x) & exists y.run(y) & exists z.see(x,z))\n"
     ]
    }
   ],
   "source": [
    "drs2 = read_dexpr('([x],[walk(x)])+([y],[run(y)])+([z],[see(x,z)])')\n",
    "show_expr(drs2)\n",
    "print(drs2.fol())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 96,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([],[(([x],[dog(x)]) -> ([y],[ankle(y), bite(x,y)]))])\nfree()= set()\n([],[(([x],[dog(x)]) -> ([y],[ankle(y), bite(x,y)]))])\nall x.(dog(x) -> exists y.(ankle(y) & bite(x,y)))\n"
     ]
    }
   ],
   "source": [
    "# 一个DRS可以内嵌入另一个DRS，这是一般量词被处理的方式\n",
    "drs3 = read_dexpr('([],[(([x],[dog(x)]) -> ([y],[ankle(y),bite(x,y)]))])')\n",
    "show_expr(drs3)\n",
    "print(drs3.fol())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 97,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([u,x,y,z],[angus(x), dog(y), own(x,y), PRO(u), irene(z), bite(u,z)])\nfree()= set()\n(([x,y],[angus(x), dog(y), own(x,y)]) + ([u,z],[PRO(u), irene(z), bite(u,z)]))\n([u,x,y,z],[angus(x), dog(y), own(x,y), (u = [x,y,z]), irene(z), bite(u,z)])\n"
     ]
    }
   ],
   "source": [
    "# DRT通过链接回指代词和现有的段落指称来解释回指代词。\n",
    "# DRT设置约束条件使段落指称可以像先行词那样“可访问”，但是并不打算解释如何从候选集合中选出特定的先行词\n",
    "# resolve_anaphora()将DRS中包括的PRO(x)形式的条件转换为x=[...]形式的条件，其中[...]是一个可能先行词的列表\n",
    "drs4 = read_dexpr('([x,y],[angus(x),dog(y),own(x,y)])')\n",
    "drs5 = read_dexpr('([u,z],[PRO(u),irene(z),bite(u,z)])')\n",
    "drs6 = drs4 + drs5\n",
    "show_expr(drs6)\n",
    "print(drs6.simplify().resolve_anaphora())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,z29],[Angus(x), dog(z29), own(x,z29)])\nfree()= set()\n([x,z29],[Angus(x), dog(z29), own(x,z29)])\n"
     ]
    }
   ],
   "source": [
    "# 对DRS的处理与 λ-抽象的处理的机制是完全兼容的，因此可以直接基于DRT而不是一阶逻辑建立组合语义表示。\n",
    "# LogicParser与DrtParser解析的结果似乎是一样的\n",
    "from nltk import load_parser\n",
    "\n",
    "parser = load_parser('grammars/book_grammars/drt.fcfg', logic_parser = nltk.sem.drt.DrtParser())\n",
    "trees = list(parser.parse('Angus owns a dog'.split()))\n",
    "show_expr(trees[0].label()['SEM'])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 111,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "β-约简= ([x,z33],[Angus(x), dog(z33), own(x,z33)])\nfree()= set()\n([x,z33],[Angus(x), dog(z33), own(x,z33)])\n"
     ]
    }
   ],
   "source": [
    "parser = load_parser('grammars/book_grammars/drt.fcfg')\n",
    "trees = list(parser.parse('Angus owns a dog'.split()))\n",
    "show_expr(trees[0].label()['SEM'])"
   ]
  },
  {
   "source": [
    "### 10.5.2 段落（话语）处理\n",
    "\n",
    "解释一句话时会利用丰富的上下文背景知识：一部分取决于前面的内容；一部分取决于背景假设。\n",
    "\n",
    "DRT提供了将句子的含义集成到前面的段落表示中的理论基础，但是缺乏：没有纳入推理；处理单个句子"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 112,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "\ns0 readings:\n\ns0-r0: exists z1.(student(z1) & dance(z1))\n\ns1 readings:\n\ns1-r0: all z1.(student(z1) -> person(z1))\n"
     ]
    }
   ],
   "source": [
    "# 使用nltk.inference.discourse来完善。\n",
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 126,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "--------------- >add sentence< ---------------\n",
      "Inconsistent discourse: d0 ['s0-r0', 's1-r0', 's2-r0']:\n",
      "    s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "    s1-r0: all z1.(student(z1) -> person(z1))\n",
      "    s2-r0: -exists z1.(person(z1) & dance(z1))\n",
      "\n",
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "\n",
      "s2 readings:\n",
      "\n",
      "s2-r0: -exists z1.(person(z1) & dance(z1))\n"
     ]
    }
   ],
   "source": [
    "# 给段落增加句子，使用“consistchk=True”就可以对加入的句子进行一致性检查\n",
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()\n",
    "show_subtitle(\"add sentence\")\n",
    "dt.add_sentence('No person dances', consistchk = True)\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 125,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "--------------- >add sentence< ---------------\n",
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "\n",
      "s2 readings:\n",
      "\n",
      "s2-r0: -exists z1.(person(z1) & dance(z1))\n"
     ]
    }
   ],
   "source": [
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()\n",
    "show_subtitle(\"add sentence\")\n",
    "dt.add_sentence('No person dances')\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 117,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "Current sentences are \ns0: A student dances\ns1: Every student is a person\n\ns0 readings:\n\ns0-r0: exists z1.(student(z1) & dance(z1))\n\ns1 readings:\n\ns1-r0: all z1.(student(z1) -> person(z1))\n"
     ]
    }
   ],
   "source": [
    "# 对于有问题的句子可以收回，“verbose = True”默认就是这个设置，输出撤回句子后的句子列表\n",
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "show_subtitle(\"add sentence\")\n",
    "dt.add_sentence('No person dances')\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()\n",
    "show_subtitle(\"retract sentence\")\n",
    "dt.retract_sentence('No person dances', verbose = True)\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 121,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >add sentence< ---------------\n",
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "\n",
      "s2 readings:\n",
      "\n",
      "s2-r0: -exists z1.(person(z1) & dance(z1))\n",
      "--------------- >retract sentence< ---------------\n",
      "Current sentences are \n",
      "s0: A student dances\n",
      "s1: Every student is a person\n",
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n"
     ]
    }
   ],
   "source": [
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "show_subtitle(\"add sentence\")\n",
    "dt.add_sentence('No person dances')\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()\n",
    "show_subtitle(\"retract sentence\")\n",
    "dt.retract_sentence('No person dances')\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 128,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "--------------- >add sentence< ---------------\n",
      "Sentence 'A person dances' under reading 'exists x.(person(x) & dance(x))':\n",
      "Not informative relative to thread 'd0'\n",
      "--------------- >reading sentence< ---------------\n",
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n",
      "\n",
      "s2 readings:\n",
      "\n",
      "s2-r0: exists z1.(person(z1) & dance(z1))\n"
     ]
    }
   ],
   "source": [
    "# 给段落增加句子，使用“informchk=True”就可以对加入的句子进行信息量检查（即是否增加了新的信息量）\n",
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "show_subtitle(\"add sentence\")\n",
    "dt.add_sentence('A person dances', informchk = True)\n",
    "show_subtitle(\"reading sentence\")\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 142,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "<Regexp Tagger: size=5>"
      ]
     },
     "metadata": {},
     "execution_count": 142
    }
   ],
   "source": [
    "# discourse模型可以适应语义歧义，筛选出不可接受的读法。\n",
    "# Glue语义模型被配置为使用覆盖面广泛的Malt依存关系分析器，输入的句子必须已经完成了分词和标注。\n",
    "# MaltParser()需要去 http://www.maltparser.org/mco/mco.html 下载 MaltParser，\n",
    "# 然后解压缩到合适的目录下，使用 parser_dirname 来设置目录\n",
    "from nltk.tag import RegexpTagger\n",
    "\n",
    "tagger = RegexpTagger([('^(chases|runs)$', 'VB'),\n",
    "                       ('^(a)$', 'ex_quant'),\n",
    "                       ('^(every)$', 'univ_quant'),\n",
    "                       ('^(dog|boy)$', 'NN'),\n",
    "                       ('^(He)$', 'PRP')])\n",
    "depparser = nltk.MaltParser(tagger = tagger,\n",
    "                            parser_dirname = 'D:\\\\Users\\\\zhuyuanxiang\\\\Library\\\\maltparser')\n",
    "rc = nltk.DrtGlueReadingCommand(depparser = depparser)\n",
    "dt = nltk.DiscourseTester(['Every dog chases a boy', 'He runs'], rc)\n",
    "# dt.readings()\n",
    "# TypeError: 'RegexpTagger' object is not callable\n",
    "# 估计是版本不匹配造成的"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 146,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "[('H', None), ('e', None), (' ', None), ('w', None), ('a', None), ('s', None), (' ', None), ('b', None), ('o', None), ('r', None), ('n', None), (' ', None), ('i', None), ('n', None), (' ', None), ('M', None), ('a', None), ('r', None), ('c', None), ('h', None), (' ', None), ('1', None), ('9', None), ('9', None), ('1', None)]\n"
     ]
    }
   ],
   "source": [
    "pattern = [(r'(March)$', 'MAR')]\n",
    "tagger = nltk.RegexpTagger(pattern)\n",
    "print(tagger.tag('He was born in March 1991'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 147,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stdout",
     "text": [
      "[('He', None), ('was', None), ('born', None), ('in', None), ('March', 'MAR'), ('1991', None)]\n"
     ]
    }
   ],
   "source": [
    "pattern = [(r'(March)$', 'MAR')]\n",
    "tagger = nltk.RegexpTagger(pattern)\n",
    "print(tagger.tag(nltk.word_tokenize('He was born in March 1991')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 158,
   "metadata": {},
   "outputs": [],
   "source": [
    "# 下面是知乎上给出的修改建议，测试了依然不行。\n",
    "# 具体可参考 https://www.zhihu.com/people/meng-hui-wei-lai-de-colin/activities\n",
    "tagger = RegexpTagger([('^(chases|runs)$', 'VB'), ('^(a)$', 'ex_quant'),\n",
    "                       ('^(every)$', 'univ_quant'), ('^(dog|boy)$', 'NN'),\n",
    "                       ('^(He)$', 'PRP')])\n",
    "depparser = nltk.MaltParser(\n",
    "    tagger=tagger.tag,\n",
    "    parser_dirname='D:\\\\Users\\\\zhuyuanxiang\\\\Library\\\\maltparser')\n",
    "rc = nltk.DrtGlueReadingCommand(depparser=depparser)\n",
    "dt = nltk.DiscourseTester(\n",
    "    [sent.split() for sent in ['Every dog chases a boy', 'He runs']], reading_command=rc)\n",
    "# dt.readings()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 159,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "[['Every', 'dog', 'chases', 'a', 'boy'], ['He', 'runs']]"
      ]
     },
     "metadata": {},
     "execution_count": 159
    }
   ],
   "source": [
    "[sent.split() for sent in ['Every dog chases a boy', 'He runs']]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 160,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "[['Every', 'dog', 'chases', 'a', 'boy'], ['He', 'runs']]"
      ]
     },
     "metadata": {},
     "execution_count": 160
    }
   ],
   "source": [
    "[nltk.word_tokenize('Every dog chases a boy'), nltk.word_tokenize('He runs')]"
   ]
  },
  {
   "source": [
    "## 10.6 小结\n",
    "\n",
    "- 一阶逻辑是一种适合在计算环境中表示自然语言含义的语言。\n",
    "    - 可以表示自然语言含义的许多方面，\n",
    "    - 还可以使用一阶逻辑失量的高效的定理证明器。\n",
    "- 将自然语言句子翻译成一阶逻辑的时候，可以通过检查一阶公式模型表述这些句子的真值条件\n",
    "- 一阶逻辑的 λ-运算，可以表示成分组合的含义\n",
    "- λ-运算中的 β-约简。\n",
    "    - 在语义上，与函数传递参数对应。\n",
    "    - 在句法上，将被函数表达式中的 λ 绑定的变量替换为函数应用中表达式提供的参数。\n",
    "- 构建模型的关键部分在于建立估值，为非逻辑常量分配解释。这些非逻辑常量可以解释为n元谓词或者独立常量\n",
    "- 开放表达式是包含一个或者多个自变量的表达式。开放表达式只在它的自变量被赋值时才能获得解释。\n",
    "- 量词的解释是对于具有变量x的公式φ[x]，构建个体的集合，赋值g分配它们作为x的值使φ[x]为真。然后量词对这个集合加以约束。\n",
    "- 封闭的表达式是没有自由变量的表达式，即变量都是被绑定的。封闭的表达式的真假取决于所有变量的赋值。\n",
    "- 如果两个公式只是由绑定操作符（即 λ 或者 量词）绑定的变量的标签不同，那么它们是 α-等价的。重新标记公式中的绑定变量的过程叫做 α-转换。\n",
    "- 给定有两个嵌套量词Q1和Q2的公式，最外层的量词Q1有比较宽的范围（或者范围超过Q2）。英语句子往往由于它们包含的量词的范围而产生歧义。\n",
    "- 在基于特征的语法中英语句子可以通过将SEM作为特征与语义表达关系。一个复杂表达式的SEM值通常包括成分表达式的SEM值的函数应用。"
   ],
   "cell_type": "markdown",
   "metadata": {}
  }
 ]
}